perm filename NSF.ADD[E77,JMC] blob
sn#303728 filedate 1977-09-07 generic text, type C, neo UTF8
COMMENT ā VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 We also see proof-checking as an essential part of our
C00006 ENDMK
Cā;
We also see proof-checking as an essential part of our
research in the epistemology of artificial intelligence. We believe
that before we try to make a computer perform a kind of reasoning,
it is valuable to be able to make it accept the reasoning. Thus, a computer
is unlikely to invent what it can't even understand.
.ss Proof-Checking by Computer
Making computers prove mathematical theorems was one of the earliest goals
of artificial intelligence research.
Indeed the general artificial intelligence problem can be reduced to the
theorem proving problem. We need only represent the facts of a problem
and the relevant facts about the world as sentences in a formal language
and write a sentence that expresses the existence of a solution to the
problem. If this sentence can be proved, there are general methods that
will usually produce a solution to the problem from a proof of its
existence. This method of doing general AI has not met with great success
for three reasons: First, we do not understand enough about how to express
facts about the world in logical languages. Second, we have not sufficiently
succeeded
in expressing the rules of reasoning accepted by people as the rules of
inference of formal systems. Third, even when the problem has been
suitably expressed in a suitable logical system, we haven't succeeded in
putting sufficiently powerful proof-search procedures in the theorem
proving programs.
The third problem - the heuristic problem of theorem proving -
has been the main focus of research in theorem proving. Over the years,
it has met with important success, and this success is responsible for
the improved performance of theorem proving programs on well-formulated
mathematical problems. The first and second problems are the main
focus of our proposed research.
The most important empirical tool for these problems is a
proof-checker. It is very easy to be fooled into believing that one
understands informal reasoning. The check comes when one expresses
the facts as sentences in a formal system and tries to make a proof-checker
accept the reasoning. The proof may be impossible if some facts have
been left out, it may be grossly too long if the formal means of reasoning
that have been provided don't correspond to the informal reasoning, and
it will be possible to prove false statements if inconsistent axioms
have been given or if excessively powerful modes of reasoning are allowed.